\begin{tabbing}
sends{-}p(${\it es}$;${\it ds}$;$k$;$T$;$l$;${\it dt}$;$g$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. es{-}vartype(${\it es}$; source($l$); $x$) $\subseteq\rho$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))\+
\\[0ex]\& (\=$\forall$$e$:es{-}E(${\it es}$).\+
\\[0ex]es{-}isrcv(${\it es}$; $e$)
\\[0ex]$\Rightarrow$ es{-}lnk(${\it es}$; $e$) $=$ $l$ $\in$ IdLnk
\\[0ex]$\Rightarrow$ es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ fpf{-}cap(${\it dt}$;IdDeq;es{-}tag(${\it es}$; $e$);Top))
\-\\[0ex]\& alle{-}at(${\it es}$;source($l$);$e$.\=es{-}kind(${\it es}$; $e$) $=$ $k$ $\in$ Knd\+
\\[0ex]$\Rightarrow$ \=es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $T$\+
\\[0ex]\& (\=$\exists$$L$:\{\=$e$:es{-}E(${\it es}$)\+\+
\\[0ex]$\mid$ \=es{-}isrcv(${\it es}$; $e$)\+
\\[0ex]\& \=es{-}lnk(${\it es}$; $e$) $=$ $l$ $\in$ IdLnk\+
\\[0ex]\& fpf{-}dom(IdDeq; es{-}tag(${\it es}$; $e$); ${\it dt}$) \} List.
\-\-\-\\[0ex]es{-}rcv{-}from(${\it es}$;$e$;$l$;$L$)
\\[0ex]\& \=map($\lambda$$e$.$\langle$es{-}tag(${\it es}$; $e$)$,\,$es{-}val(${\it es}$; $e$)$\rangle$;$L$)\+
\\[0ex]$=$
\\[0ex]concat(map\=(\=$\lambda$${\it tgf}$.\+\+
\\[0ex]sends{-}msgs(es{-}state{-}when(${\it es}$;$e$);es{-}val
\\[0ex](${\it es}$; $e$);${\it tgf}$)
\-\\[0ex];$g$))
\-\\[0ex]$\in$ (${\it tg}$:Id$\times$fpf{-}cap(${\it dt}$;IdDeq;${\it tg}$;Void)) List))
\-\-\-\-\-
\end{tabbing}